Search results for " Proving"

showing 10 items of 10 documents

Argumentation and proving: a didactical experience with Chinese and Italian students

2009

Argumentation and proving chinese studentsSettore MAT/04 - Matematiche Complementari
researchProduct

Argumentation and Proving in Multicultural Classes: A didactical experience with Chinese and Italian students

2009

Argumentation Proving Multicultural ChineseSettore MAT/04 - Matematiche Complementari
researchProduct

Different procedures in argumentation and conjecturation in primary school:an experience with Chinese students

2008

Chinese students argumentation and provingSettore MAT/04 - Matematiche Complementari
researchProduct

Integrated Simulation and Formal Verification of a Simple Autonomous Vehicle

2018

This paper presents a proof-of-concept application of an approach to system development based on the integration of formal verification and co-simulation. A simple autonomous vehicle has the task of reaching an assigned straight path and then follow it, and it can be controlled by varying its turning speed. The correctness of the proposed control law has been formalized and verified by interactive theorem proving with the Prototype Verification System. Concurrently, the system has been co-simulated using the Prototype Verification System and the MathWorks Simulink tool: The vehicle kinematics have been simulated in Simulink, whereas the controller has been modeled in the logic language of t…

CorrectnessSIMPLE (military communications protocol)Computer scienceProof assistant020207 software engineeringControl engineering02 engineering and technologyFormal methods Software engineering Theorem proving Vehicles Autonomous Vehicles Control laws Integrated simulations Interactive theorem proving Logic languages Proof of concept Prototype verification systems System development020202 computer hardware & architectureAutomated theorem provingSettore ING-INF/04 - AutomaticaControl theory0202 electrical engineering electronic engineering information engineeringPrototype Verification SystemFormal verificationLogic programming
researchProduct

Survey of Formal Verification Methods for Smart Contracts on Blockchain

2019

Due to the immutable nature of distributed ledger technology such as blockchain, it is of utter importance that a smart contract works as intended before employment outside test network. This is since any bugs or errors will become permanent once published to the live network, and could lead to substantial economic losses; as manifested in the infamous DAO smart contract exploit hack in 2016. In order to avoid this, formal verification methods can be used to ensure that the contract behaves according to given specifications. This paper presents a survey of the state of the art of formal verification of smart contracts. Being a relatively new research area, a standard or best practice for fo…

Model checkingSmart contractExploitComputer science020206 networking & telecommunications02 engineering and technologyFormal methodsComputer securitycomputer.software_genreSyntax (logic)Automated theorem provingOrder (business)0202 electrical engineering electronic engineering information engineering020201 artificial intelligence & image processingFormal verificationcomputer2019 10th IFIP International Conference on New Technologies, Mobility and Security (NTMS)
researchProduct

Block-Based Models and Theorem Proving in Model-Based Development

2021

This paper presents a methodology to integrate computer-assisted theorem proving into a standard workflow for model-based development that uses a block-based language as a modeling and simulation tool. The theorem prover provides confidence in the results of the analysis as it guides the developers towards a correct formalization of the system under development.

PVStheorem provingModel-based developmentMatlab; Model-based development; PVS; theorem provingMatlab
researchProduct

Reasoning and proving in Algebra. Examples from 8th grade school mathematics textbooks in Italy

2022

Some research studies concerning the didactics of Algebra discuss how learning to solve problems using symbolic algebraic language can be hard for students (Bohlmann et al., 2014; Palm, 2009). Students, in fact, have often difficulty to learn the ways in which the sym- bols should be manipulated to argue or to prove an assertion in order to reach a problem solu- tions. Although many studies conducted by mathematics educators discussed important contri- butions to this subject (e.g. Arzarello, Robutti & Bazzini, 2005; Boero, 2001; Carraher, Schliemann, Brizuela & Earnest, 2006; Lins & Kaput, 2004; Ursini & Trigueros, 2001), not many analysis were conducted on the role of the …

Settore MAT/04 - Matematiche ComplementariReasoning Proving Algebra school mathematics textbooks
researchProduct

The Italian Method of la drammatica: its Legacy and Reception

2014

The volume The Italian Method of la drammatica: its Legacy and Reception includes the long and complex investigation to identify the Italian acting-code system of the drammatica used by nineteenth-century Italian actors such as Adelaide Ristori Giovanni Grasso Tommaso Salvini Eleonora Duse. In particular their acting inspired Stanislavky who reformed twentieth-century stage. The declamatory code of the drammatica was composed by symbols for notation of voice and gesture which Italian actors marked in their prompt-books. The discovery of the drammatica’s code sheds new light on nineteenth-century acting. Having deciphered the phonetic symbols of the code Anna Sica has given birth an investigation with a group of outstanding scholars in an attempt to explore the drammatica’s legacy and its reception in Europe as well as in Asia. At this stage new evidence has emerged proving that for instance the symbol used by the drammatica actors to sign the colorito vocale was known to English actors in the second half of the nineteenth century. By noting how Adelaide Ristori passed on her art to Irving’s actress Genevieve Ward and how Stanislavsky almost aflame moulded his system from Duse’s acting an unexplored variety in the reception of the drammatica’s legacy is revealed.Settore L-ART/05 - Discipline Dello Spettacolo
researchProduct

Le società in house nel quadro della nozione europea e nazionale di impresa di gruppo

2020

L’articolo si propone di ricostruire in chiave sistematica il concetto di “società in house” nell’ambito del quadro della nozione europea e nazionale di impresa di gruppo. Ricondurre la relazione in house ad un rapporto di gruppo tra due o più imprese dovrebbe comportare, in prima battuta, l’applicazione della cd. single economic entity doctrine e delle sue ricadute in ambito concorrenziale, fra le quali acquista particolare rilievo la potenziale imputazione delle sanzioni antitrust all’ente pubblico capogruppo per le infrazioni compiute dalle società eterodirette. Nell’ordinamento giuridico nazionale, inoltre, la sostanziale convergenza tra il tipo di controllo alla base dell’in house prov…

single economic entity doctrinein-house proving companiegroup of companieSettore IUS/04 - Diritto Commerciale
researchProduct

Continuum: A spatiotemporal data model to represent and qualify filiation relationships

2013

International audience; This work introduces an ontology-based spatio-temporal data model to represent entities evolving in space and time. A dynamic phenomenon generates a complex relationship network between the entities involved in the process. At the abstract level, the relationships can be identity or topological filiations. The existence of an identity filiation depends on whether the object changes its identity or not. On the other hand, topological filiations are based exclusively on the spatial component, like in the case of growth, reduction, merging or splitting. When combining identity and topological filiations, six filiation relationships are obtained, forming a second abstrac…

spatial dynamicsTheoretical computer sciencefiliationintegrity constraintsSpatio-temporal modelingspatio-temporal evolutionComputer scienceOntology (information science)Object (computer science)computer.software_genreSemantic data modelConsistency (database systems)[ INFO.INFO-HC ] Computer Science [cs]/Human-Computer Interaction [cs.HC]Data modelData integrityI.2.4 [ARTIFICIAL INTELLIGENCE]: Knowledge Representation Formalisms and Methods - Semantic networks. I.2.3 [ARTIFICIAL INTELLIGENCE]: Deduction and Theorem Proving - Inference engines.Identity (object-oriented programming)semanticreasoningData mining[INFO.INFO-HC]Computer Science [cs]/Human-Computer Interaction [cs.HC][INFO.INFO-HC] Computer Science [cs]/Human-Computer Interaction [cs.HC]computerSemantic Web
researchProduct